\begin{tabbing}
$\forall$\=${\it es}$:ES, $A$:Type, $i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]${\it conds}$:$k$:Knd fp$\rightarrow$ $V$:Type $\times$ (State(${\it ds}$)$\rightarrow$$V$$\rightarrow$($A$ + Top)).
\-\\[0ex]($\forall$$k$:Knd. ($\uparrow$$k$ $\in$ dom(${\it conds}$)) $\Rightarrow$ ($\uparrow$hasloc($k$;$i$)))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex](loc($e$) = $i$)
\\[0ex]$\Rightarrow$ ($\uparrow$kind($e$) $\in$ dom(${\it conds}$))
\\[0ex]$\Rightarrow$ \=((valtype($e$) $\subseteq$r (${\it conds}$(kind($e$)).1))\+
\\[0ex]\& (($\exists$$k$:Knd. ($\uparrow$$k$ $\in$ dom(${\it conds}$))) $\Rightarrow$ (state@loc($e$) $\subseteq$r State(${\it ds}$)))))
\-\-\\[0ex]$\Rightarrow$ (es{-}triggers(${\it es}$;$i$;${\it ds}$;${\it conds}$) $\in$ AbsInterface($A$))
\end{tabbing}